home *** CD-ROM | disk | FTP | other *** search
/ Celestin Apprentice 2 / Apprentice-Release2.iso / Tools / Languages / Caml Light 0.61 / Source / src / compiler / typing.ml < prev    next >
Encoding:
Text File  |  1994-07-07  |  12.8 KB  |  414 lines  |  [TEXT/MPS ]

  1. (* typing.ml : type inference *)
  2.  
  3. #open "misc";;
  4. #open "const";;
  5. #open "globals";;
  6. #open "syntax";;
  7. #open "builtins";;
  8. #open "modules";;
  9. #open "types";;
  10. #open "errors";;
  11. #open "ty_error";;
  12.  
  13. (* To convert type expressions to types *)
  14.  
  15. let type_expr_vars =
  16.   ref ([] : (string * typ) list);;
  17.  
  18. let reset_type_expression_vars () =
  19.   type_expr_vars := []
  20. ;;
  21.  
  22. let bind_type_expression_vars var_list =
  23.   type_expr_vars := [];
  24.   map
  25.     (fun v ->
  26.       if mem_assoc v !type_expr_vars then
  27.         failwith "bind_type_expression_vars"
  28.       else begin
  29.         let t = new_type_var() in
  30.           type_expr_vars := (v, t) :: !type_expr_vars; t
  31.       end)
  32.     var_list
  33. ;;
  34.  
  35. let type_of_type_expression strict_flag typexp =
  36.   let rec type_of = function
  37.     Typexp(Ztypevar v, _) ->
  38.       begin try
  39.         assoc v !type_expr_vars
  40.       with Not_found ->
  41.         if strict_flag then
  42.           unbound_type_var_err v typexp
  43.         else begin
  44.           let t = new_type_var() in
  45.           type_expr_vars := (v,t) :: !type_expr_vars; t
  46.         end
  47.       end
  48.   | Typexp(Ztypearrow(arg1, arg2), loc) ->
  49.       type_arrow(type_of arg1, type_of arg2)
  50.   | Typexp(Ztypetuple argl, loc) ->
  51.       type_product(map type_of argl)
  52.   | Typexp(Ztypeconstr(cstr_name, args), loc) as texp ->
  53.       let cstr =
  54.         try
  55.           find_type_desc cstr_name
  56.         with Desc_not_found ->
  57.           unbound_err "Type constructor" cstr_name loc in
  58.       if list_length args != cstr.info.ty_arity then
  59.         type_arity_err cstr args loc;
  60.       { typ_desc=Tconstr(cstr.info.ty_constr, map type_of args);
  61.         typ_level=notgeneric }
  62.   in type_of typexp
  63. ;;
  64.  
  65. (* Typing of constants *)
  66.  
  67. let type_of_atomic_constant = function
  68.     ACint _ -> type_int
  69.   | ACfloat _ -> type_float
  70.   | ACstring _ -> type_string
  71.   | ACchar _ -> type_char
  72. ;;
  73.  
  74. let rec type_of_structured_constant = function
  75.     SCatom ac ->
  76.       type_of_atomic_constant ac
  77.   | SCblock(cstr, args) ->
  78.       fatal_error "type_of_structured_constant" (* to do? *)
  79. ;;
  80.  
  81. (* Typing of patterns *)
  82.  
  83. let unify_pat pat ty ty' =
  84.   try
  85.     unify (ty, ty')
  86.   with Unify ->
  87.     pat_wrong_type_err pat ty' ty
  88. ;;
  89.  
  90. let rec tpat new_env ((Pat(desc, loc) as pat), ty, mut_flag) =
  91.   match desc with
  92.     Zwildpat ->
  93.       new_env
  94.   | Zvarpat v ->
  95.       if mem_assoc v new_env then
  96.         non_linear_pattern_err pat v
  97.       else
  98.         (v, (ty, mut_flag)) :: new_env
  99.   | Zaliaspat(pat, v) ->
  100.       if mem_assoc v new_env then
  101.         non_linear_pattern_err pat v
  102.       else
  103.         tpat ((v, (ty, mut_flag)) :: new_env) (pat, ty, mut_flag)
  104.   | Zconstantpat cst ->
  105.       unify_pat pat ty (type_of_atomic_constant cst);
  106.       new_env
  107.   | Ztuplepat(patl) ->
  108.       begin try
  109.         tpat_list new_env patl (filter_product (list_length patl) ty)
  110.       with Unify ->
  111.         pat_wrong_type_err pat ty
  112.           (type_product(new_type_var_list (list_length patl)))
  113.       end
  114.   | Zconstruct0pat(cstr) ->
  115.       begin match cstr.info.cs_kind with
  116.         Constr_constant ->
  117.           unify_pat pat ty (type_instance cstr.info.cs_res);
  118.           new_env
  119.       | _ ->
  120.           non_constant_constr_err cstr loc
  121.       end
  122.   | Zconstruct1pat(cstr, arg) ->
  123.       begin match cstr.info.cs_kind with
  124.         Constr_constant ->
  125.           constant_constr_err cstr loc
  126.       | _ ->
  127.         let (ty_res, ty_arg) =
  128.           type_pair_instance (cstr.info.cs_res, cstr.info.cs_arg) in
  129.         unify_pat pat ty ty_res;
  130.         tpat new_env (arg, ty_arg, cstr.info.cs_mut)
  131.       end
  132.   | Zorpat(pat1, pat2) ->
  133.       begin match free_vars_of_pat pat with
  134.         [] -> tpat (tpat new_env (pat1, ty, mut_flag)) (pat2, ty, mut_flag)
  135.       | _  -> orpat_should_be_closed_err pat
  136.       end
  137.   | Zconstraintpat(pat, ty_expr) ->
  138.       let ty' = type_of_type_expression false ty_expr in
  139.       let new_env' = tpat new_env (pat, ty', mut_flag) in
  140.         unify_pat pat ty ty';
  141.         new_env'
  142.   | Zrecordpat lbl_pat_list ->
  143.       let rec tpat_lbl new_env = function
  144.         [] -> new_env
  145.       | (lbl,p) :: rest ->
  146.           let (ty_res, ty_arg) =
  147.             type_pair_instance (lbl.info.lbl_res, lbl.info.lbl_arg) in
  148.           unify_pat pat ty ty_res;
  149.           tpat_lbl (tpat new_env (p, ty_arg, lbl.info.lbl_mut)) rest
  150.       in
  151.         tpat_lbl new_env lbl_pat_list
  152.  
  153. and tpat_list new_env = fun
  154.     [] [] ->
  155.       new_env
  156.   | (pat::patl) (ty::tyl) ->
  157.       tpat_list (tpat new_env (pat, ty, Notmutable)) patl tyl
  158.   | _ _ ->
  159.       fatal_error "type_pattern: arity error"
  160. ;;
  161.  
  162. let type_pattern = tpat []
  163. and type_pattern_list = tpat_list []
  164. and type_pattern_list2 = it_list tpat []
  165. ;;
  166.  
  167. (* Typing of expressions *)
  168.  
  169. let unify_expr expr ty ty' =
  170.   try
  171.     unify (ty, ty')
  172.   with Unify ->
  173.     expr_wrong_type_err expr ty' ty
  174. ;;
  175.  
  176. let rec type_expr env =
  177.   let rec texp ((Expr(desc, loc) as expr), ty) =
  178.     match desc with
  179.       Zident r ->
  180.         let ty' =
  181.           match !r with
  182.             Zglobal glob_desc ->
  183.               type_instance glob_desc.info.val_typ
  184.           | Zlocal s ->
  185.               try
  186.                 let (ty_schema, mut_flag) = assoc s env in
  187.                   type_instance ty_schema
  188.               with Not_found ->
  189.                 try
  190.                   let glob_desc = find_value_desc(GRname s) in
  191.                     r := Zglobal glob_desc;
  192.                     type_instance glob_desc.info.val_typ
  193.                 with Desc_not_found ->
  194.                   unbound_err "Variable" (GRname s) loc
  195.         in
  196.           unify_expr expr ty ty'
  197.     | Zconstant cst ->
  198.         unify_expr expr ty (type_of_structured_constant cst)
  199.     | Ztuple(args) ->
  200.         begin try
  201.           texp_list (args, filter_product (list_length args) ty)
  202.         with Unify ->
  203.           expr_wrong_type_err expr
  204.             (type_product(new_type_var_list (list_length args))) ty
  205.         end
  206.     | Zconstruct0(cstr) ->
  207.         begin match cstr.info.cs_kind with
  208.           Constr_constant ->
  209.             unify_expr expr ty (type_instance cstr.info.cs_res)
  210.         | _ ->
  211.             non_constant_constr_err cstr loc
  212.         end            
  213.     | Zconstruct1(cstr, arg) ->
  214.         begin match cstr.info.cs_kind with
  215.           Constr_constant ->
  216.             constant_constr_err cstr loc
  217.         | _ ->            
  218.             let (ty_res, ty_arg) =
  219.               type_pair_instance (cstr.info.cs_res, cstr.info.cs_arg) in
  220.             unify_expr expr ty ty_res;
  221.             texp(arg, ty_arg)
  222.         end
  223.     | Zapply(fct, args) ->
  224.         let rec make_ty_fct = function
  225.           [] -> ([], ty)
  226.         | arg1::argl ->
  227.             let alpha = new_type_var()
  228.             and (ty_args, ty_fct) = make_ty_fct argl
  229.             in (alpha::ty_args, type_arrow(alpha, ty_fct)) in
  230.         let (ty_args, ty_fct) = make_ty_fct args in
  231.           texp(fct, ty_fct);
  232.           texp_list(args, ty_args)
  233.     | Zlet(rec_flag, pat_expr_list, body) ->
  234.         type_expr (type_let_decl env rec_flag pat_expr_list) (body, ty)
  235.     | Zfunction [] ->
  236.         fatal_error "type_expr: empty matching"
  237.     | Zfunction ((casel1,expr1)::_ as matching) ->
  238.         let rec find_types ty = function
  239.           [] -> ([],ty)
  240.         | pat::rest ->
  241.             try
  242.               let (ty1,ty2) = filter_arrow ty in
  243.               let (ty_args, ty_res) = find_types ty2 rest in
  244.                 (ty1 :: ty_args, ty_res)
  245.             with Unify ->
  246.               expr_wrong_type_err expr
  247.                  (type_arrow(new_type_var(), new_type_var())) ty in
  248.         let (ty_args, ty_res) =
  249.           find_types ty casel1 in
  250.         let tcase (patl, expr) =
  251.           if list_length patl != list_length ty_args then
  252.             ill_shaped_match_err expr;
  253.           type_expr (type_pattern_list patl ty_args @ env) (expr, ty_res)
  254.         in
  255.           do_list tcase matching
  256.     | Ztrywith (body, matching) ->
  257.         texp (body, ty);
  258.         do_list
  259.           (fun (pat, expr) ->
  260.             type_expr (type_pattern (pat, type_exn, Notmutable) @ env)
  261.                       (expr, ty))
  262.           matching
  263.     | Zsequence (e1, e2) ->
  264.         type_statement env e1; texp(e2, ty)
  265.     | Zcondition (cond, ifso, ifnot) ->
  266.         texp(cond, type_bool);
  267.         texp(ifnot, ty);
  268.         texp(ifso, ty)
  269.     | Zwhile (cond, body) ->
  270.         texp(cond, type_bool);
  271.         type_statement env body;
  272.         unify_expr expr ty type_unit
  273.     | Zfor (id, start, stop, up_flag, body) ->
  274.         texp(start, type_int);
  275.         texp(stop, type_int);
  276.         type_statement ((id,(type_int,Notmutable)) :: env) body;
  277.         unify_expr expr ty type_unit
  278.     | Zsequand (e1, e2) ->
  279.         texp(e1, type_bool);
  280.         texp(e2, type_bool);
  281.         unify_expr expr ty type_bool
  282.     | Zsequor (e1, e2) ->
  283.         texp(e1, type_bool);
  284.         texp(e2, type_bool);
  285.         unify_expr expr ty type_bool
  286.     | Zconstraint (e, ty_expr) ->
  287.         let ty' = type_of_type_expression false ty_expr in
  288.           texp(e, ty');
  289.           unify_expr expr ty ty'
  290.     | Zvector elist ->
  291.         let ty_arg = new_type_var() in
  292.         let ty_vect = type_vect ty_arg in
  293.         unify_expr expr ty ty_vect;
  294.         do_list (fun e -> texp(e, ty_arg)) elist
  295.     | Zassign(id, e) ->
  296.         begin try
  297.           match assoc id env with
  298.             (ty_schema, Notmutable) ->
  299.               not_mutable_err id loc
  300.           | (ty_schema, Mutable) ->
  301.               unify_expr expr ty type_unit;
  302.               texp (e, type_instance ty_schema)
  303.         with Not_found ->
  304.           unbound_err "The local variable" (GRname id) loc
  305.         end
  306.     | Zrecord lbl_expr_list ->
  307.         do_list
  308.           (fun (lbl, e) ->
  309.             let (ty_res, ty_arg) =
  310.               type_pair_instance (lbl.info.lbl_res, lbl.info.lbl_arg) in
  311.             unify_expr expr ty ty_res;
  312.             texp (e, ty_arg))
  313.           lbl_expr_list;
  314.         let label_list = labels_of_type ty in
  315.         let v = make_vect (list_length label_list) false in
  316.           do_list (fun (lbl, e) ->
  317.             let p = lbl.info.lbl_pos in
  318.               if v.(p)
  319.               then label_err " is multiply defined." expr lbl
  320.               else v.(p) <- true)
  321.             lbl_expr_list;
  322.           let rec check_labels i = function
  323.             [] -> ()
  324.           | lbl::rest ->
  325.               if v.(i)
  326.               then check_labels (succ i) rest
  327.               else label_err " is undefined." expr lbl
  328.           in check_labels 0 label_list
  329.     | Zrecord_access (e, lbl) ->
  330.         let (ty_res, ty_arg) =
  331.           type_pair_instance (lbl.info.lbl_res, lbl.info.lbl_arg) in
  332.         unify_expr expr ty ty_arg;
  333.         texp(e, ty_res)
  334.     | Zrecord_update (e1, lbl, e2) ->
  335.         let (ty_res, ty_arg) =
  336.           type_pair_instance (lbl.info.lbl_res, lbl.info.lbl_arg) in
  337.         unify_expr expr ty type_unit;
  338.         if lbl.info.lbl_mut == Notmutable then
  339.           label_err " is not mutable." expr lbl;
  340.         texp(e1, ty_res);
  341.         texp(e2, ty_arg)
  342.     | Zstream complist ->
  343.         let ty_comp = new_type_var() in
  344.         unify_expr expr ty (type_stream ty_comp);
  345.         do_list
  346.           (function Zterm e -> texp(e, ty_comp)
  347.                   | Znonterm e -> texp(e, ty))
  348.           complist
  349.     | Zparser casel ->
  350.         let ty_comp = new_type_var() in
  351.         let ty_stream = type_stream ty_comp in
  352.         let ty_res = new_type_var() in
  353.         unify_expr expr ty (type_arrow(ty_stream, ty_res));
  354.         let rec type_stream_pat new_env = function
  355.           ([], act) ->
  356.             type_expr (new_env @ env) (act, ty_res)
  357.         | (Ztermpat p :: rest, act) ->
  358.             type_stream_pat (tpat new_env (p, ty_comp, Notmutable)) (rest,act)
  359.         | (Znontermpat(parsexpr,p) :: rest, act) ->
  360.             let ty_parser_result = new_type_var() in
  361.             type_expr (new_env @ env)
  362.                       (parsexpr, type_arrow(ty_stream, ty_parser_result));
  363.             type_stream_pat (tpat new_env (p, ty_parser_result, Notmutable))
  364.                             (rest,act)
  365.         | (Zstreampat s :: rest, act) ->
  366.             type_stream_pat ((s, (ty_stream, Notmutable)) :: new_env) (rest,act)
  367.         in
  368.         do_list (type_stream_pat [])  casel
  369.  
  370.   and texp_list = function
  371.     [], [] -> ()
  372.   | e::el, ty::tyl ->
  373.       texp(e,ty); texp_list(el,tyl)
  374.   | _ ->
  375.       fatal_error "texp_list"
  376.  
  377.   in texp
  378.  
  379. (* Typing of "let" definitions *)
  380.  
  381. and type_let_decl env rec_flag pat_expr_list =
  382.   push_type_level();
  383.   let (pat_ty_list, expr_ty_list) =
  384.     list_it
  385.      (fun (pat,expr) (pt, et) ->
  386.         let alpha = new_type_var () in
  387.           (pat,alpha,Notmutable)::pt, (expr,alpha)::et)
  388.      pat_expr_list
  389.      ([],[]) in
  390.   let add_env =
  391.     type_pattern_list2 pat_ty_list in
  392.   let new_env =
  393.     add_env @ env
  394.   in
  395.     do_list
  396.       (type_expr (if rec_flag then new_env else env))
  397.       expr_ty_list;
  398.     pop_type_level();
  399.     do_list (fun (_, (ty, _)) -> generalize_type ty) add_env;
  400.    new_env
  401.  
  402. (* Typing of statements (expressions whose value is ignored) *)
  403.  
  404. and type_statement env (Expr(desc, loc) as e) =
  405.   let ty = new_type_var() in
  406.   type_expr env (e, ty);
  407.   match (type_repr ty).typ_desc with
  408.     Tarrow(_,_) ->
  409.       location__prerr_location loc;
  410.       prerr_begline " Warning: function partially applied.";
  411.       prerr_endline2 ""
  412.   | _ -> ()
  413. ;;
  414.